\begin{tabbing}
$\forall$${\it es}$:ES, $A$:Type, $R$:(E$\rightarrow$$A$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. Dec($\exists$$a$:$A$. $R$($e$,$a$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$X$:AbsInterface($A$)\+
\\[0ex]($\forall$$e$:E. (($\uparrow$($e$ $\in_{b}$ $X$)) $\Leftarrow\!\Rightarrow$ ($\exists$$a$:$A$. $R$($e$,$a$))) \& (($\uparrow$($e$ $\in_{b}$ $X$)) $\Rightarrow$ $R$($e$,$X$($e$)))))
\-
\end{tabbing}